$\forall$${\it es}$:ES, $i$:Id, $P$:(state@$i$$\rightarrow$Prop).
\\[0ex]@$i$ stable ${\it state}$.$P$(${\it state}$)  
\\[0ex]$\Rightarrow$ $\forall$$e$@$i$. $P$(state after $e$) $\Rightarrow$ ($\forall$${\it e'}$:E. ($e$ $<$loc ${\it e'}$) $\Rightarrow$ $P$((state when ${\it e'}$)))